%include
:- lib(ic), lib(listut).

testDateIsLeapYear(Path, OState, Arg, Result, NState) :-
	Path > 0,
	% Domains
	[ODay] :: -127 .. 128,
	[NDay] :: -127 .. 128,
	[OMonth] :: -127 .. 128,
	[NMonth] :: -127 .. 128,
	[OYear] :: -127 .. 128,
	[NYear] :: -127 .. 128,
	% Constraints
	OState = [ODay, OMonth, OYear],
	NState = [NDay, NMonth, NYear],
	dateIsLeapYear(Path, OState, Arg, Result, NState),
	% Solving
	indomain(ODay),
	indomain(NDay),
	indomain(OMonth),
	indomain(NMonth),
	indomain(OYear),
	indomain(NYear).

dateIsLeapYear(1, [ODay, OMonth, OYear], [], Result, [NDay, NMonth, NYear]) :-
	% Invariant
	ODay #> 0,
	OMonth #> 0,
	OYear #> 0,
	% Postcondition
	NYear mod 4 #= 0,
	neg(NYear mod 100 #= 0),
	neg(NYear mod 400 #= 0),
	Result = 'false',
	NYear #= OYear,
	NMonth #= OMonth,
	NDay #= ODay,
	% Object State Update
	NDay #= ODay,
	NMonth #= OMonth,
	NYear #= OYear,
	% Invariant
	NDay #> 0,
	NMonth #> 0,
	NYear #> 0.

